(set-logic QF_BV)
(declare-fun _substvar_1579_ () Bool)
(declare-fun _substvar_1580_ () Bool)
(declare-fun _substvar_2755_ () Bool)
(declare-fun _substvar_2788_ () Bool)
(declare-fun _substvar_2939_ () Bool)
(declare-fun _substvar_3446_ () Bool)
(declare-fun _substvar_4448_ () Bool)
(declare-fun _substvar_4449_ () Bool)
(declare-fun operator1 () (_ BitVec 4))
(declare-fun opr1_1 () (_ BitVec 4))
(declare-fun op1_1 () (_ BitVec 4))
(declare-fun opr1_3 () (_ BitVec 4))
(declare-fun op1_3 () (_ BitVec 4))
(declare-fun op3_1 () (_ BitVec 4))
(declare-fun operator4 () (_ BitVec 4))
(declare-fun opr4_1 () (_ BitVec 4))
(declare-fun op4_1 () (_ BitVec 4))
(declare-fun opr4_3 () (_ BitVec 4))
(declare-fun op4_3 () (_ BitVec 4))
(declare-fun decode_1 () (_ BitVec 17))
(declare-fun func_1 () (_ BitVec 1))
(declare-fun out_2 () (_ BitVec 4))
(declare-fun decode_3 () (_ BitVec 17))
(declare-fun out_3 () (_ BitVec 4))
(assert (let ((?v_8 (= opr1_1 operator1)) (?v_9 false) (?v_3 true) (?v_0 true) (?v_1 true) (?v_2 (= opr4_1 operator4)) (?v_10 true) (?v_4 true) (?v_11 true) (?v_5 true) (?v_6 true) (?v_7 true) (?v_12 false) (?v_13 true) (?v_14 _substvar_1580_) (?v_15 (= func_1 (_ bv0 1))) (?v_16 ((_ extract 15 12) decode_1)) (?v_17 (_ bv0 4)) (?v_18 (_ bv0 4)) (?v_19 ((_ extract 3 0) decode_1)) (?v_28 true) (?v_23 true) (?v_20 true) (?v_21 true) (?v_22 true) (?v_24 true) (?v_25 true) (?v_26 true) (?v_27 true) (?v_29 true) (?v_30 true) (?v_31 true) (?v_32 (_ bv0 4)) (?v_33 false) (?v_34 (_ bv0 4)) (?v_35 (_ bv0 4)) (?v_36 (_ bv0 4)) (?v_45 (= opr1_3 operator1)) (?v_40 true) (?v_37 _substvar_4448_) (?v_38 true) (?v_39 (= opr4_3 operator4)) (?v_41 _substvar_4449_) (?v_42 true) (?v_43 false) (?v_44 true) (?v_46 true) (?v_47 true) (?v_48 _substvar_2788_) (?v_49 ((_ extract 16 13) decode_3)) (?v_50 (_ bv0 4)) (?v_51 true) (?v_52 (_ bv0 4)) (?v_53 ((_ extract 3 0) decode_3))) (and ?v_8 (= opr4_1 operator4) ?v_8 _substvar_1579_ (ite _substvar_1580_ (= decode_1 (concat (concat (concat (concat (_ bv0 1) opr1_1) (_ bv0 4)) (_ bv0 4)) opr4_1)) (= decode_1 (concat (concat (concat (concat (_ bv0 1) opr4_1) (_ bv0 4)) (_ bv0 4)) opr1_1))) (ite _substvar_1580_ (and ?v_15 (= op1_1 ?v_16) _substvar_2939_ (= op3_1 (_ bv0 4)) (= op4_1 ?v_19)) (and ?v_15 (= op4_1 ?v_16) _substvar_2755_ (= op1_1 ?v_19))) (ite (= func_1 (_ bv1 1)) (= (_ bv0 4) (bvadd op1_1 op4_1)) (= (_ bv0 4) (bvor (bvor op1_1 op3_1) op4_1))) (= out_2 (_ bv0 4)) ?v_45 (ite false false (and _substvar_4449_ _substvar_4448_ (= opr4_3 operator4))) ?v_45 (ite _substvar_2788_ (= decode_3 (concat (concat (concat (concat opr1_3 (_ bv0 4)) (_ bv0 1)) (_ bv0 4)) opr4_3)) (= decode_3 (_ bv0 17))) (ite _substvar_2788_ (and (= op1_3 ((_ extract 16 13) decode_3)) _substvar_3446_ (= op4_3 ((_ extract 3 0) decode_3))) false) (= out_3 (bvor op1_3 op4_3)) (not (= out_2 out_3)))))
(check-sat)
(exit)
